$\forall$${\it es}$:ES, $T$:Type, $x$:Id, $e_{1}$, $e_{2}$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} , $P$:($T$$\rightarrow\mathbb{P}$).
\\[0ex]$\forall$$e$$\in$[$e_{1}$,$e_{2}$).$P$(($x$ after $e$)) $\Leftarrow\!\Rightarrow$ $\forall$$e$$\in$($e_{1}$,$e_{2}$].$P$($x$ when $e$)